es:ES{i}, i:Id, L:(IdLnk List), T:(IdType{i}).
es-secret-server{table:ut2, encrypt:ut2, decrypt:ut2}(es; T; L; i)  {i'} 

latex

Definitions	DeclaredType(ds;x), tt, if b then t else f fi , Top, x. t(x), e@i. P(e), s.x, A c B, data(T), P & Q, secret-table(T), "$x", let x = a in b(x), es-secret-server, , t  T, IdLnk, Id, x:A. B(x), S  T, P  Q, , State(ds), x(s), i  j < k, {i..j}
Lemmas	event system wf, IdLnk wf, Id wf, st-encrypt wf, effect-p wf, subtype rel self, fpf-cap wf, es-val wf, es-vartype wf, eqof eq btrue, id-deq wf, fpf-cap-single, es-when wf, st-decrypt wf, fpf-single wf, es-kind-sends-iff wf, l all wf, es-isconst wf, assert wf, unit wf, st-length wf, int seg wf, le wf, st-next wf, deq wf, fpf-cap-single1